Nuprl Lemma : es-is-le-interface
11,40
postcript
pdf
es
:ES,
X
:AbsInterface(Top),
e
:E. (
(
e
le(
X
)))
(
e'
:E. (
e'
loc
e
& (
(
e'
X
))))
latex
Definitions
P
Q
,
t
T
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
E
,
x
:
A
B
(
x
)
,
P
&
Q
,
b
,
s
=
t
,
Top
,
ES
,
AbsInterface(
A
)
,
P
Q
,
e
X
,
x
.
A
(
x
)
Lemmas
es-interface
wf
,
event
system
wf
,
es-local-le-pred-property
,
es-E
wf
,
top
wf
,
es-is-interface
wf
origin
es:ES, X:AbsInterface(Top), e:E. (
(e 
le(X))) 
(
e':E. (e' 
loc e & ((e' X)))) es:ES, X:AbsInterface(Top), e:E. ((e le(X))) (e':E. (e' loc e & ((e' X)))) Q T
B(x)x:A. B(x)
B(x)b Q X
x.A(x)